|
In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by〔 Here:sect.2.1, p. 250〕 :''s'' ≤ ''t'' if a subterm of ''t'' is a substitution instance of ''s''. It is used e.g. in the Knuth–Bendix completion algorithm. ==Properties== * Encompassment is a preorder, i.e. reflexive and transitive, but not anti-symmetric,〔since both ''f''(''x'') ≤ ''f''(''y'') and ''f''(''y'') ≤ ''f''(''x'') for variable symbols ''x'', ''y'' and a function symbol ''f''〕 nor total〔since neither ''a'' ≤ ''b'' nor ''b'' ≤ ''a'' for distinct constant symbols ''a'', ''b''〕 * The corresponding equivalence relation, defined by ''s'' ~ ''t'' if ''s'' ≤ ''t'' ≤ ''s'', is equality modulo renaming. * ''s'' ≤ ''t'' whenever ''s'' is a subterm of ''t''. * ''s'' ≤ ''t'' whenever ''t'' is a substitution instance of ''s''. * The union of any well-founded rewrite order ''R''〔i.e. irreflexive, transitive, and well-founded binary relation ''R'' such that ''sRt'' implies ''u''(HREF="http://www.kotoba.ne.jp/word/11/Substitution (logic)#First-order logic" TITLE="Substitution (logic)#First-order logic">σ )''p'' R ''u''()''p'' for all terms ''s'', ''t'', ''u'', each path ''p'' of ''u'', and each substitution ''σ''〕 with (<) is well-founded, where (<) denotes the irreflexive kernel of (≤).〔Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, ''R'' is required to be a "terminating rewrite relation" there.〕 In particular, (<) itself is well-founded. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Encompassment ordering」の詳細全文を読む スポンサード リンク
|